Termination Proof Script
Consider the TRS R consisting of the rewrite rules
1:
ap
(
f
,x)
→ x
2:
ap
(
ap
(
ap
(
g
,x),y),
ap
(
s
,z))
→
ap
(
ap
(
ap
(
g
,x),y),
ap
(
ap
(x,y),
0
))
There are 3 dependency pairs:
3:
AP
(
ap
(
ap
(
g
,x),y),
ap
(
s
,z))
→
AP
(
ap
(
ap
(
g
,x),y),
ap
(
ap
(x,y),
0
))
4:
AP
(
ap
(
ap
(
g
,x),y),
ap
(
s
,z))
→
AP
(
ap
(x,y),
0
)
5:
AP
(
ap
(
ap
(
g
,x),y),
ap
(
s
,z))
→
AP
(x,y)
The approximated dependency graph contains one SCC: {3,5}.
Consider the SCC {3,5}.
The constraints could not be solved.
Tyrolean Termination Tool
(0.02 seconds) --- May 3, 2006